<html>
<head>
  <title>abrance</title>
  <basefont face="Consolas" size="2" />
  <meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
  <meta name="exporter-version" content="YXBJ Windows/602326 (zh-CN, DDL); Windows/10.0.0 (Win64); EDAMVersion=V2;"/>
  <style>
    body, td {
      font-family: Consolas;
      font-size: 10pt;
    }
  </style>
</head>
<script type="text/javascript" src="https://cdn.bootcdn.net/ajax/libs/jquery/1.11.3/jquery.js"></script><script> $(function () {console.log($("a").attr("target", "_blank"));})</script>
<body>
<a name="3604"/>
<h1>λ演算</h1>
<div>
<table bgcolor="#D4DDE5" border="0">
<tr><td><b>创建时间：</b></td><td><i>2020/11/13 14:48</i></td></tr>
<tr><td><b>更新时间：</b></td><td><i>2020/11/13 15:25</i></td></tr>
<tr><td><b>作者：</b></td><td><i>DaguguJ</i></td></tr>
<tr><td><b>标签：</b></td><td><i>lambda</i></td></tr>
</table>
</div>
<br/>

<div>
<span><div><div><br/></div><table style="border-collapse: collapse; min-width: 100%;"><colgroup><col style="width: 193px;"></col><col style="width: 1017px;"></col></colgroup><tbody><tr><td style="width: 193px; padding: 8px; border: 1px solid;"><div>λ演算</div></td><td style="width: 1017px; padding: 8px; border: 1px solid;"><div><br/></div></td></tr><tr><td style="width: 193px; padding: 8px; border: 1px solid;"><div>参考</div></td><td style="width: 1017px; padding: 8px; border: 1px solid;"><ul><li><div><a href="https://www.jianshu.com/p/ebae04e1e47c">https://www.jianshu.com/p/ebae04e1e47c</a></div></li></ul></td></tr><tr><td style="width: 193px; padding: 8px; border: 1px solid;"><div>lambda | λ 定义</div></td><td style="width: 1017px; padding: 8px; border: 1px solid;"><ul><li><div><span style="font-size: unset; color: unset; font-family: unset;">要描述一个形式系统，我们首先需要约定用到的基本符号，对于本系列所介绍的lambda演算，其符号集包括λ . ()和变量名(x, y, z, etc.)</span></div></li></ul></td></tr><tr><td style="width: 193px; padding: 8px; border: 1px solid;"><div><br/></div></td><td style="width: 1017px; padding: 8px; border: 1px solid;"><ul><li><div>一个λ式 只有一个参数，多个参数需要currying 化</div></li></ul></td></tr><tr><td style="width: 193px; padding: 8px; border: 1px solid;"><div>1. λ 表达式/项</div></td><td style="width: 1017px; padding: 8px; border: 1px solid;"><ul><li><div><span style="color: unset; font-family: unset; font-size: unset;">在lambda演算中只有三种合法表达式（也可以称之为项：λ-expression or λ-term）存在：</span><br/></div></li><li><div>变量(Variable)</div></li><ul><li><div>形式：x</div></li><li><div>变量名可能是一个字符或字符串，它表示一个参数（形参）或者一个值（实参）。</div></li><li><div>e.g. z var</div></li></ul><li><div>抽象(Abstraction)</div></li><ul><li><div>形式：λx.M</div></li><li><div>它表示获取一个参数x并返回M的lambda函数，M是一个合法lambda表达式，且符号λ和.表示绑定变量x于该函数抽象的函数体M。简单来说就是表示一个形参为x的函数M。</div></li><li><div>e.g. λx.y λx.(λy.xy)</div></li><li><div>前者表示一个常量函数(constant function)，输出恒为y与输入无关；后者的输出是一个函数抽象λy.xy，输入可以是任意的lambda表达式。</div></li><li><div>注意：一个lambda函数的输入和输出也可以是函数。</div></li></ul><li><div>应用(Application)</div></li><li><div>形式：M N</div></li><ul><li><div>它表示将函数M应用于参数N，其中M、N均为合法lambda表达式。简单来说就是给函数M输入实参N。</div></li><li><div>e.g. (λx.x) y, (λx.x) (λx.x)</div></li><li><div>前者表示将函数λx.x应用于变量y，得到y；后者表示将函数λx.x应用于λx.x，得到λx.x。函数λx.x是一个恒等函数(identity function)，即输入恒等于输出，它可以用 I 来表示。</div></li></ul><li><div>这时候可能就有人纳闷儿了，(λx.x) y意义很明确，但λy.xy为什么代表函数抽象而不是将函数λy.x应用于y的函数应用呢？为了消除类似的表达式歧义，可以多使用小括号，也有以下几个消歧约定可以参考：</div></li><ul><li><div>* 一个函数抽象的函数体将尽最大可能向右扩展，即：λx.M N代表的是一个函数抽象λx.(M N)而非函数应用(λx.M) N。</div></li><li><div>* 函数应用是左结合的，即：M N P意为(M N) P而非M (N P)。</div></li></ul></ul></td></tr><tr><td style="width: 193px; padding: 8px; border: 1px solid;"><div>2. 自由变量和绑定变量</div></td><td style="width: 1017px; padding: 8px; border: 1px solid;"><ul><li><div><span style="color: unset; font-family: unset; font-size: unset;">前面提到在函数抽象中，形参绑定于函数体，即形参是绑定变量，相对应地，不是绑定变量的自然就是自由变量。咱们来通过几个例子来理解这个关系：</span><br/></div></li></ul><ul><ul><li><div>λx.xy：其中x是绑定变量，y是自由变量；</div></li><li><div>(λy.y)(λx.xy)：这个表达式可以按括号划分为两个子表达式M和N，M的y是绑定变量，无自由变量，N的x是绑定变量，y是自由变量且与M无关；</div></li><li><div>λx.(λy.xyz)：这个表达式中的x绑定于外部表达式，y绑定于内部表达式，z是自由变量。</div></li></ul><li><div>由于每个lambda函数都只有一个参数，因此也只有一个绑定变量，这个绑定变量随着形参的变化而变化。</div></li><li><div>我们用FV来表示一个lambda表达式中所有自由变量的集合，如：</div></li><ul><li><div>FV(λx.xy) = {y}</div></li><li><div>FV((λy.y)(λx.xy)) = FV(λy.y) ∪ FV(λx.xy) = {y}</div></li><li><div>FV(λx.(λy.xyz)) = FV(λy.xyz) \ x = {x,z} \ x = {z}</div></li></ul></ul></td></tr><tr><td style="width: 193px; padding: 8px; border: 1px solid;"><div>3.柯里化(Currying)</div></td><td style="width: 1017px; padding: 8px; border: 1px solid;"><ul><li><div><span style="color: unset; font-family: unset; font-size: unset;">有时候我们的函数需要有多个参数，这太正常不过了，但是lambda函数只能有一个参数？解决这个问题的方法就是柯里化(Currying)。</span><br/></div></li></ul><ul><li><div>柯里化是用于处理多参数输入情况的方法，我们已经知道一个lambda函数的输入和输出也可以是函数，那么基于它，可以把多参数函数和单参数函数做以下转换：</div></li><li><div>currying: λx y.xy = λx.(λy.xy)</div></li><li><div>外层函数接受一个参数x返回一个函数λy.xy，这个返回函数（内层函数）又接受一个参数y返回xy，x绑定于外层函数，y绑定于内层函数，这样我们就在满足lambda函数只接受一个参数的约束下实现了多参数函数的功能，这就是柯里化，而λx y.xy称为λx.(λy.xy)的缩写，为了方便表达，后续会常常出现λx y.xy这样的书写方式，需要谨记它只是缩写写法</div></li></ul></td></tr><tr><td style="width: 193px; padding: 8px; border: 1px solid;"><div><br/></div></td><td style="width: 1017px; padding: 8px; border: 1px solid;"><div><br/></div></td></tr><tr><td style="width: 193px; padding: 8px; border: 1px solid;"><div>lambda | λ 归约</div></td><td style="width: 1017px; padding: 8px; border: 1px solid;"><ul><li><div><span style="color: unset; font-family: unset; font-size: unset;">我们已经知道了lambda表达式的基本定义与语法，下面将介绍如何对一个lambda表达式进行归约(reduction)。</span></div></li></ul></td></tr><tr><td style="width: 193px; padding: 8px; border: 1px solid;"><div>1. beta | β 归约</div></td><td style="width: 1017px; padding: 8px; border: 1px solid;"><ul><li><div>对于一个函数应用(λx.x) y，它意为将函数应用λx.x应用于y，等价于x[x:=y]，即结果是y。在这个过程中，(λx.x) y ≡ x[x:=y]一步就叫做beta归约，x[x:=y] ≡ y一步称作替换(substitution)，<font style="color: rgb(188, 0, 88);">[x:=y]意为将表达式中的自由变量x替换为y</font>。</div></li><li><div>* 替换</div></li><ul><li><div>形式：E[V := R]</div></li><li><div>意为将表达式E中的所有 “自由变量” V替换为表达式R。对于变量x,y和lambda表达式M,N，有以下规则：</div></li><li><div>x[x := N]       ≡ N</div></li><li><div>y[x := N]       ≡ y //注意 x ≠ y(M1 M2)[x := N] ≡ (M1[x := N]) (M2[x := N])(λx.M)[x := N]  ≡ λx.M //注意 x 是绑定变量无法替换(λy.M)[x := N]  ≡ λy.(M[x := N]) //注意 x ≠ y, 且表达式N的自由变量中不包含 y 即 y ∉ FV(N)</div></li></ul><li><div>* beta归约</div></li><ul><li><div>形式：β: ((λV.E) E′) ≡ E[V := E′]</div></li><li><div>其实就是用实参替换函数体中的形参，也就是函数抽象应用(apply)于参数的过程啦，只不过这个参数除了是一个变量还可能是一个表达式。</div></li><li><div>细心的话可以注意到，替换规则中特别标注了一些x ≠ y或者y ∉ FV(N)等约束条件，它们的意义在于防止lambda表达式的归约过程中出现歧义。</div></li></ul><li><div>eg：</div></li><ul><li><div>(λx.(λy.xy)) y</div></li><li><div>= (λy.xy)[x:=y] //beta归约：注意 y ∈ FV(y) 不满足替换的约束条件= λy.yy //替换：绑定变量y与自由变量y同名出现了冲突</div></li><li><div>可以看出在不满足约束条件的情况强行替换造成了错误的结果，需要alpha转换。</div></li></ul></ul></td></tr><tr><td style="width: 193px; padding: 8px; border: 1px solid;"><div>2. alpha | α 转换</div></td><td style="width: 1017px; padding: 8px; border: 1px solid;"><ul><li><div><span style="color: unset; font-family: unset; font-size: unset;">这条规则表明：一个lambda函数抽象在更名绑定变量前后是等价的，即：</span><br/></div></li><ul><li><div>α: λx.x ≡ λy.y</div></li></ul><li><div>其作用就是解决绑定变量与自由变量间的同名冲突问题。</div></li><li><div>那么对于上面的那个错误归约过程纠正一下了：</div></li><ul><li><div>(λx.(λy.xy))y</div></li><li><div>= (λy.xy)[x:=y] //beta归约：注意 y ∈ FV(y) 不满足替换的约束条件= (λz.xz)[x:=y] //alpha转换：因为绑定变量y将与自由变量x（将被替换为y）冲突，所以更名为z= λz.yz</div></li></ul></ul></td></tr><tr><td style="width: 193px; padding: 8px; border: 1px solid;"><div>3. eta | η 归约</div></td><td style="width: 1017px; padding: 8px; border: 1px solid;"><ul><li><div><span style="color: unset; font-family: unset; font-size: unset;">灵活运用alpha和beta已经可以解决所有的lambda表达式归约问题，但是考虑这样一个表达式：</span><br/></div></li><ul><li><div>λx.M x</div></li></ul><li><div>将它应用于任意一个参数上，比如(λx.M x) N，进行beta归约和替换后会发现它等价于M N，这岂不是意味着</div></li><ul><li><div>λx.M x ≡ M</div></li></ul><li><div>对于形如λx.M x，其中表达式M不包含绑定变量x的函数抽象，它是冗余的，等价于M，而这就是eta归约，它一般用于清除lambda表达式中存在的冗余函数抽象。</div></li></ul></td></tr><tr><td style="width: 193px; padding: 8px; border: 1px solid;"><div><br/></div></td><td style="width: 1017px; padding: 8px; border: 1px solid;"><div><br/></div></td></tr></tbody></table><div><br/></div></div><div><br/></div></span>
</div></body></html> 